(set-option :incremental false)
(set-info :source "MathSat group")
(set-info :status unsat)
(set-info :category "random")
(set-info :difficulty "3")
(set-logic QF_UFLRA)
(declare-fun f0_1 (Real) Real)
(declare-fun f0_2 (Real Real) Real)
(declare-fun f0_3 (Real Real Real) Real)
(declare-fun f0_4 (Real Real Real Real) Real)
(declare-fun f1_1 (Real) Real)
(declare-fun f1_2 (Real Real) Real)
(declare-fun f1_3 (Real Real Real) Real)
(declare-fun f1_4 (Real Real Real Real) Real)
(declare-fun x0 () Real)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun x4 () Real)
(declare-fun x5 () Real)
(declare-fun x6 () Real)
(declare-fun x7 () Real)
(declare-fun x8 () Real)
(declare-fun x9 () Real)
(declare-fun P0 () Bool)
(declare-fun P1 () Bool)
(declare-fun P2 () Bool)
(declare-fun P3 () Bool)
(declare-fun P4 () Bool)
(declare-fun P5 () Bool)
(declare-fun P6 () Bool)
(declare-fun P7 () Bool)
(declare-fun P8 () Bool)
(declare-fun P9 () Bool)
(check-sat-assuming ( (let ((_let_0 (f0_1 x3))) (let ((_let_1 (* 9.0 x9))) (let ((_let_2 (* 15.0 x3))) (let ((_let_3 (- (+ (* 29.0 x6) (* 21.0 x7)) (* 25.0 x9)))) (let ((_let_4 (- (+ (* (/ (- 0 27) 1) x1) (* 23.0 x9)) (* 22.0 x5)))) (let ((_let_5 (f0_2 (+ (+ (* (/ (- 0 18) 1) x6) (* 13.0 x5)) (* 2.0 x7)) x6))) (let ((_let_6 (f1_1 x7))) (let ((_let_7 (- (+ (* 26.0 _let_0) (* 24.0 _let_5)) (* 6.0 x7)))) (let ((_let_8 (f1_2 x8 x5))) (let ((_let_9 (f1_1 (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6))))) (let ((_let_10 (f1_2 x7 x4))) (let ((_let_11 (+ (+ (* 27.0 x7) (* 22.0 x9)) (* 24.0 x6)))) (let ((_let_12 (+ (+ (* 15.0 x2) (* 6.0 x5)) (* 10.0 x9)))) (let ((_let_13 (- 0 5))) (let ((_let_14 (< (+ (- (* (/ (- 0 13) 1) x3) (* 8.0 x9)) (* 6.0 x4)) (/ _let_13 1)))) (let ((_let_15 (< (f0_2 _let_5 _let_10) (/ (- 0 26) 1)))) (let ((_let_16 (< (f0_2 x8 x7) 6.0))) (let ((_let_17 (< (+ (- (* 13.0 x0) _let_2) (* 6.0 x2)) 20.0))) (let ((_let_18 (< x4 (/ (- 0 27) 1)))) (let ((_let_19 (- 0 25))) (let ((_let_20 (< _let_12 (/ _let_19 1)))) (let ((_let_21 (< (f0_2 _let_9 _let_8) (/ (- 0 28) 1)))) (let ((_let_22 (< (- (- (* (/ (- 0 9) 1) x1) (* 22.0 x3)) (* 19.0 x8)) 10.0))) (let ((_let_23 (< _let_4 9.0))) (let ((_let_24 (< _let_7 (/ _let_13 1)))) (let ((_let_25 (< _let_4 28.0))) (let ((_let_26 (< x5 (/ (- 0 12) 1)))) (let ((_let_27 (< _let_11 16.0))) (let ((_let_28 (= (+ (+ (* 16.0 x0) (* 10.0 x1)) _let_2) _let_0))) (let ((_let_29 (< x5 14.0))) (let ((_let_30 (= (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6)) (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6))))) (let ((_let_31 (< _let_12 (/ (- 0 23) 1)))) (let ((_let_32 (= _let_7 _let_11))) (let ((_let_33 (< (- (- (* (/ (- 0 9) 1) x1) (* 22.0 x3)) (* 19.0 x8)) 12.0))) (let ((_let_34 (< x1 (/ (- 0 4) 1)))) (let ((_let_35 (< x1 29.0))) (let ((_let_36 (< _let_7 8.0))) (let ((_let_37 (< _let_3 (/ (- 0 26) 1)))) (let ((_let_38 (< (f1_2 x5 x0) 0.0))) (let ((_let_39 (= x4 (- (+ (* 18.0 x2) _let_1) (* 7.0 x6))))) (let ((_let_40 (< (f0_2 x1 x6) 9.0))) (let ((_let_41 (< (- (- (* 24.0 x6) _let_1) (* 13.0 x5)) (/ (- 0 8) 1)))) (let ((_let_42 (< (- (- (* (/ (- 0 9) 1) x1) (* 22.0 x3)) (* 19.0 x8)) (/ (- 0 18) 1)))) (let ((_let_43 (< (f0_2 x8 x7) 11.0))) (let ((_let_44 (= (f0_2 (- (- (* (/ (- 0 11) 1) x9) (* 21.0 x4)) (* 11.0 x7)) (f0_1 x4)) _let_12))) (let ((_let_45 (< _let_10 (/ (- 0 22) 1)))) (let ((_let_46 (< (f1_2 x8 x6) (/ (- 0 3) 1)))) (let ((_let_47 (not _let_42))) (let ((_let_48 (not _let_28))) (let ((_let_49 (not _let_41))) (let ((_let_50 (not _let_20))) (let ((_let_51 (not (< (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6)) (/ (- 0 20) 1))))) (let ((_let_52 (not _let_26))) (let ((_let_53 (not (< _let_7 13.0)))) (let ((_let_54 (not (< _let_8 15.0)))) (let ((_let_55 (not _let_15))) (let ((_let_56 (not _let_33))) (let ((_let_57 (not (< _let_3 26.0)))) (let ((_let_58 (not (< x7 (/ (- 0 22) 1))))) (let ((_let_59 (not (= (f1_2 x8 x6) (- (- (* (/ (- 0 11) 1) x9) (* 21.0 x4)) (* 11.0 x7)))))) (let ((_let_60 (not _let_36))) (let ((_let_61 (not (= _let_9 (f0_2 _let_5 _let_10))))) (let ((_let_62 (not _let_31))) (let ((_let_63 (not _let_32))) (let ((_let_64 (not _let_22))) (let ((_let_65 (or _let_45 _let_24))) (let ((_let_66 (not _let_30))) (let ((_let_67 (not _let_39))) (let ((_let_68 (not (= (f1_2 x7 x0) (+ (- (* 13.0 x0) _let_2) (* 6.0 x2)))))) (let ((_let_69 (not _let_27))) (let ((_let_70 (not (< (f0_2 (- (- (* (/ (- 0 11) 1) x9) (* 21.0 x4)) (* 11.0 x7)) (f0_1 x4)) (/ (- 0 11) 1))))) (let ((_let_71 (not _let_16))) (let ((_let_72 (not (< x6 6.0)))) (let ((_let_73 (not _let_46))) (let ((_let_74 (not _let_38))) (let ((_let_75 (not (< (f0_1 x4) 10.0)))) (let ((_let_76 (not _let_21))) (let ((_let_77 (not _let_43))) (let ((_let_78 (not (< _let_11 (/ (- 0 6) 1))))) (let ((_let_79 (not _let_37))) (let ((_let_80 (not _let_29))) (let ((_let_81 (not (< _let_10 4.0)))) (let ((_let_82 (not (< _let_6 10.0)))) (let ((_let_83 (or _let_50 _let_42))) (let ((_let_84 (not _let_45))) (let ((_let_85 (not _let_17))) (let ((_let_86 (not _let_35))) (let ((_let_87 (not _let_14))) (let ((_let_88 (not (= (f1_2 x0 x7) (f0_2 x1 x0))))) (let ((_let_89 (not _let_24))) (let ((_let_90 (not _let_23))) (let ((_let_91 (not (< (+ (+ (* 7.0 x5) (* 15.0 x5)) (* 24.0 x0)) (/ _let_19 1))))) (let ((_let_92 (not _let_34))) (let ((_let_93 (not _let_25))) (let ((_let_94 (not _let_40))) (let ((_let_95 (not _let_44))) (let ((_let_96 (or _let_38 _let_75))) (let ((_let_97 (not (< _let_6 (/ _let_19 1))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not P8) _let_27) (< _let_11 (/ (- 0 6) 1))) (or (or (not P2) _let_43) _let_47)) (or (or (not P8) _let_20) _let_48)) (or (or _let_49 _let_50) _let_51)) (or (or _let_52 (< _let_10 4.0)) _let_53)) (or (or _let_43 _let_54) _let_32)) (or (or _let_30 _let_20) _let_55)) (or (or _let_56 _let_50) (< (+ (+ (* 7.0 x5) (* 15.0 x5)) (* 24.0 x0)) (/ _let_19 1)))) (or (or _let_34 (< x6 6.0)) P4)) (or (or (< _let_11 (/ (- 0 6) 1)) (not P7)) (< _let_8 15.0))) (or (or P4 _let_36) _let_15)) (or (or _let_25 P7) _let_57)) (or (or _let_55 _let_58) _let_59)) (or (or _let_57 _let_57) (< _let_6 (/ _let_19 1)))) (or (or _let_39 (< _let_10 4.0)) _let_60)) (or (or _let_49 _let_27) _let_61)) (or (or _let_49 _let_25) _let_57)) (or (or _let_60 _let_62) _let_63)) (or (or _let_64 _let_63) _let_29)) (or (or _let_53 _let_61) _let_15)) (or (or _let_49 (not _let_18)) _let_24)) (or _let_65 (< _let_6 10.0))) (or (or _let_27 _let_37) _let_66)) (or (or (not P8) _let_67) _let_68)) (or (or _let_47 _let_69) _let_70)) (or (or _let_59 _let_71) _let_63)) (or (or _let_48 _let_31) _let_72)) (or (or (< x7 (/ (- 0 22) 1)) (= _let_9 (f0_2 _let_5 _let_10))) _let_48)) (or (or _let_73 _let_60) _let_74)) (or (or _let_68 _let_73) P3)) (or (or (not P5) _let_73) _let_43)) (or (or _let_42 (= (f1_2 x0 x7) (f0_2 x1 x0))) _let_75)) (or (or _let_22 _let_36) _let_76)) (or (or _let_52 _let_77) _let_66)) (or (or _let_39 _let_33) _let_43)) (or (or _let_17 _let_30) _let_59)) (or (or P3 _let_37) _let_49)) (or (or _let_39 _let_78) _let_57)) (or (or _let_79 (= (f1_2 x0 x7) (f0_2 x1 x0))) _let_72)) (or (or _let_80 _let_37) _let_41)) (or (or _let_81 _let_76) _let_33)) (or (or _let_69 P8) _let_29)) (or (or _let_46 (not P2)) _let_31)) (or (or _let_15 _let_82) P2)) (or (or _let_36 _let_41) _let_62)) (or (or _let_21 _let_36) P0)) (or _let_83 _let_80)) (or (or P0 _let_84) _let_55)) (or (or _let_51 _let_14) _let_35)) (or (or _let_85 _let_86) _let_64)) (or (or _let_36 P8) _let_21)) (or (or _let_64 P3) _let_32)) (or (or P5 _let_78) _let_87)) (or (or _let_59 _let_48) _let_37)) (or (or _let_40 _let_88) (< x6 6.0))) (or (or (< _let_3 26.0) _let_64) _let_89)) (or (or (not P0) _let_59) (< (+ (+ (* 7.0 x5) (* 15.0 x5)) (* 24.0 x0)) (/ _let_19 1)))) (or (or (= (f1_2 x8 x6) (- (- (* (/ (- 0 11) 1) x9) (* 21.0 x4)) (* 11.0 x7))) _let_38) (not P7))) (or (or _let_57 _let_67) _let_69)) (or (or _let_77 _let_22) _let_36)) (or (or _let_70 (= _let_9 (f0_2 _let_5 _let_10))) _let_76)) (or (or (not P1) (< _let_10 4.0)) _let_79)) (or (or _let_87 (< _let_3 26.0)) _let_36)) (or (or _let_85 _let_60) (< (f0_1 x4) 10.0))) (or (or P0 _let_36) _let_32)) (or (or _let_63 _let_60) _let_67)) (or (or P0 _let_76) _let_71)) (or (or _let_17 _let_44) _let_46)) (or (or _let_42 _let_44) _let_71)) (or (or (< x7 (/ (- 0 22) 1)) (< _let_6 (/ _let_19 1))) _let_52)) (or (or (not P4) _let_41) _let_35)) (or (or _let_32 _let_79) _let_46)) (or (or (= (f1_2 x0 x7) (f0_2 x1 x0)) (not P1)) _let_62)) (or (or (not P2) (< x6 6.0)) _let_24)) (or (or P3 _let_40) (< (f0_1 x4) 10.0))) (or (or _let_27 _let_55) (< _let_6 (/ _let_19 1)))) (or (or _let_63 (< _let_6 (/ _let_19 1))) _let_22)) (or (or _let_68 _let_20) _let_90)) (or (or _let_53 _let_29) _let_46)) (or (or _let_91 (< _let_6 10.0)) _let_79)) (or (or _let_70 _let_30) _let_63)) (or (or _let_90 _let_89) _let_54)) (or (or _let_84 _let_54) (< (f0_1 x4) 10.0))) (or (or _let_32 _let_39) _let_21)) (or (or _let_32 _let_24) _let_91)) (or (or _let_30 (< _let_6 (/ _let_19 1))) _let_47)) (or (or _let_49 _let_35) _let_92)) (or (or (not P7) _let_62) _let_54)) (or (or _let_86 _let_32) _let_69)) (or (or _let_80 (< _let_3 26.0)) _let_73)) (or (or _let_37 (< (f0_1 x4) 10.0)) _let_22)) (or (or (= (f1_2 x8 x6) (- (- (* (/ (- 0 11) 1) x9) (* 21.0 x4)) (* 11.0 x7))) (not P4)) _let_18)) (or (or _let_17 _let_32) _let_20)) (or (or _let_47 (not P4)) _let_67)) (or (or _let_49 (< (f0_2 (- (- (* (/ (- 0 11) 1) x9) (* 21.0 x4)) (* 11.0 x7)) (f0_1 x4)) (/ (- 0 11) 1))) _let_69)) (or (or _let_53 (< _let_6 10.0)) _let_20)) (or (or _let_84 _let_91) _let_68)) (or (or _let_71 _let_17) (not P7))) (or (or (< (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6)) (/ (- 0 20) 1)) _let_28) _let_93)) (or (or _let_30 (not P4)) P8)) (or (or _let_23 P9) _let_58)) (or (or _let_75 _let_44) _let_53)) (or (or (< x6 6.0) _let_68) (< _let_11 (/ (- 0 6) 1)))) (or (or _let_89 (< _let_6 10.0)) P1)) (or (or _let_15 _let_72) (not P9))) (or (or _let_85 _let_85) (< x7 (/ (- 0 22) 1)))) (or (or _let_33 (not P9)) _let_71)) (or (or _let_85 _let_78) _let_74)) (or (or _let_50 (not P7)) _let_57)) (or (or _let_77 _let_43) P5)) (or (or _let_22 _let_28) _let_54)) (or (or _let_41 _let_26) (< x6 6.0))) (or (or _let_27 _let_30) _let_69)) (or (or P0 _let_81) _let_46)) (or (or (< (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6)) (/ (- 0 20) 1)) _let_45) _let_69)) (or (or _let_72 _let_28) _let_87)) (or _let_65 (not P1))) (or (or P5 _let_25) _let_15)) (or (or (not P8) _let_94) _let_95)) (or (or _let_26 (not P3)) _let_69)) (or (or _let_73 P5) (not P0))) (or (or _let_16 P2) _let_27)) (or (or _let_23 _let_46) _let_84)) (or (or _let_40 _let_55) (< _let_11 (/ (- 0 6) 1)))) (or (or _let_23 _let_85) (< _let_7 13.0))) (or (or (not P0) _let_89) _let_40)) (or (or _let_49 _let_18) _let_68)) (or (or _let_68 (< _let_6 10.0)) _let_78)) (or (or _let_73 _let_39) _let_26)) (or _let_96 _let_52)) (or (or _let_40 P6) _let_62)) (or (or _let_60 P1) _let_61)) (or (or (not P0) _let_69) _let_30)) (or (or _let_58 (not P3)) _let_82)) (or (or _let_81 (< (f0_1 x4) 10.0)) _let_39)) (or (or (not P5) _let_87) _let_36)) (or (or _let_35 _let_16) _let_38)) (or (or _let_45 _let_75) _let_29)) (or (or _let_34 P1) _let_44)) (or (or _let_60 _let_70) (not P2))) (or _let_83 _let_18)) (or (or (< _let_8 15.0) _let_89) P7)) (or (or _let_69 _let_69) (not P5))) (or (or _let_53 _let_45) _let_95)) (or (or P7 P9) _let_18)) (or (or _let_57 (< _let_6 10.0)) _let_50)) (or (or P8 _let_59) _let_82)) (or (or _let_25 _let_70) P5)) (or (or _let_18 (< _let_7 13.0)) _let_97)) (or (or (not P7) _let_85) _let_23)) (or (or _let_25 _let_36) P3)) (or (or _let_63 (< (f0_1 x4) 10.0)) (< _let_10 4.0))) (or (or P7 _let_39) _let_54)) (or (or _let_94 _let_70) _let_60)) (or (or P8 _let_92) P7)) (or (or _let_59 (not P1)) (not P4))) (or (or _let_44 (< _let_10 4.0)) _let_26)) (or (or _let_92 P3) _let_88)) (or (or _let_61 P1) _let_95)) (or (or _let_25 P1) _let_24)) (or (or _let_59 (< (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6)) (/ (- 0 20) 1))) P9)) (or (or _let_56 _let_34) _let_82)) (or (or _let_97 _let_53) _let_31)) (or (or P0 _let_93) (not P8))) (or (or _let_54 _let_92) (not P8))) (or (or P7 P4) (< (- (+ (* 26.0 x3) (* 17.0 x5)) (* 1.0 x6)) (/ (- 0 20) 1)))) (or (or _let_78 _let_51) _let_84)) (or (or (< (+ (+ (* 7.0 x5) (* 15.0 x5)) (* 24.0 x0)) (/ _let_19 1)) _let_53) _let_63)) (or (or _let_46 _let_29) P2)) (or (or _let_49 _let_63) _let_36)) (or (or _let_79 _let_31) _let_15)) (or (or _let_17 _let_88) _let_94)) (or (or _let_29 P2) _let_91)) (or (or _let_74 _let_87) _let_41)) (or (or _let_32 _let_57) _let_75)) (or (or _let_76 _let_34) (not P4))) (or (or _let_31 _let_14) _let_49)) (or (or _let_81 _let_34) _let_40)) (or (or _let_50 _let_28) _let_27)) (or (or _let_50 _let_59) _let_36)) (or (or _let_91 _let_16) _let_15)) (or (or P5 _let_91) (not P1))) (or (or _let_28 _let_80) (not P5))) (or (or _let_66 _let_90) _let_33)) (or (or _let_94 P2) _let_46)) (or (or _let_23 _let_52) _let_16)) (or (or _let_63 _let_58) _let_89)) (or (or (not P8) _let_46) _let_51)) (or (or _let_42 _let_34) _let_22)) (or (or _let_72 _let_45) _let_86)) (or (or _let_32 _let_20) _let_82)) (or (or (not P1) _let_25) _let_73)) (or (or _let_72 P2) _let_40)) (or (or _let_55 _let_62) _let_78)) (or (or _let_27 _let_28) P7)) (or (or _let_28 _let_51) _let_38)) (or (or _let_85 _let_22) P8)) (or (or _let_16 _let_45) P5)) (or (or _let_60 _let_81) _let_39)) (or _let_96 _let_28)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))
